00100	∀(X1)(SET(X1)→CLASS(X1));
00200	
00300	∀(X1,X2)(ELEMENT(X1,X2)→SET(X1));
00400	
00500	∀(X1,X2)(∀(X3)(SET(X3)→(ELEMENT(X3,X1)↔ELEMENT(X3,X2)))→EQU(X1,X2));
00600	
00700	∀(X1)(SET(X1)→(∀(X2)(SET(X2)→(∃(X3)(SET(X3)∧(∀(X4)(SET(X4)→
00800	(ELEMENT(X4,X3)↔(EQU(X4,X1)∨EQU(X4,X2))))))))));
00900	
01000	∃(X1)∀(X2)(SET(X2)→∀(X3)(SET(X3)→(ELEMENT(ORDPAIR(X2,X3),X1)↔
01100	ELEMENT(X2,X3))));
01200	
01300	∀(X1,X2)∃(X3)∀(X4)(SET(X4)→(ELEMENT(X4,X3)↔(ELEMENT(X4,X1)∧
01400	ELEMENT(X4,X2))));
01500	
01600	∀(X1)∃(X2)∀(X3)(SET(X3)→(ELEMENT(X3,X2)↔(¬ELEMENT(X3,X1))));
01700	
01800	∀(X1)∃(X2)∀(X3)(SET(X3)→(ELEMENT(X3,X2)↔∃(X4)ELEMENT(ORDPAIR(X4,X3),X1)));
01900	
02000	∀(X1)∃(X2)∀(X3)(SET(X3)→∀(X4)(SET(X4)→(ELEMENT(TUPLE2(X4,X3),X2)↔
02100	ELEMENT(X3,X1))));
02200	
02300	∀(X1)∃(X2)∀(X3)(SET(X3)→∀(X4)(SET(X4)→(ELEMENT(TUPLE2(X3,X4),X2)↔
02400	ELEMENT(TUPLE2(X4,X3),X1))));
02500	
02600	∀(X1)∃(X2)∀(X3)(SET(X3)→∀(X4)(SET(X4)→∀(X5)(SET(X5)→
02700	(ELEMENT(TUPLE3(X3,X4,X5),X2)↔ELEMENT(TUPLE3(X4,X5,X3),X1)))));
02800	
02900	∀(X1)∃(X2)∀(X3)(SET(X3)→∀(X4)(SET(X4)→∀(X5)(SET(X5)→
03000	(ELEMENT(TUPLE3(X3,X4,X5),X2)↔ELEMENT(TUPLE3(X3,X5,X4),X1)))));
03100	
03200	∃(X1)(SET(X1)∧(¬EMPTY(X1)∧∀(X2)(SET(X2)→(ELEMENT(X2,X1)→
03300	∃(X3)(ELEMENT(X3,X1)∧PROPSUBSET(X2,X3))))));
03400	
03500	∀(X1)(SET(X1)→∃(X2)(SET(X2)∧∀(X3)(SET(X3)→∀(X4)(SET(X4)→
03600	((ELEMENT(X3,X4)∧ELEMENT(X4,X1))→ELEMENT(X3,X2))))));
03700	
03800	∀(X1)(SET(X1)→∃(X2)(SET(X2)∧∀(X3)(SET(X3)→
03900	(SUBSET(X3,X1)→ELEMENT(X3,X2)))));
04000	
04100	∀(X1)(SET(X1)→∀(X2)(ONEMANY(X2)→∃(X3)(SET(X3)∧∀(X4)(SET(X4)→
04200	(ELEMENT(X4,X3)↔∃(X5)(SET(X5)∧(ELEMENT(X5,X1)∧
04300	ELEMENT(TUPLE2(X4,X5),X2))))))));
04400	
04500	∀(X1)(¬EMPTY(X1)→∃(X2)(SET(X2)∧(ELEMENT(X2,X1)∧DISJOINT(X2,X1))));
04600	
04700	∃(X1)(ONEMANY(X1)∧∀(X2)(SET(X2)→(¬EMPTY(X2)→∃(X3)(SET(X3)∧
04800	(ELEMENT(X3,X2)∧ELEMENT(TUPLE2(X3,X2),X1))))));
04900	
05000	∀(X1,X2)(SUBSET(X1,X2)↔∀(X3)(SET(X3)→(ELEMENT(X3,X1)→ELEMENT(X3,X2))));
05100	
05200	∀(X1,X2)(PROPSUBSET(X1,X2)↔(SUBSET(X1,X2)∧¬EQU(X1,X2)));
05300	
05400	∀(X1)(EMPTY(X1)↔∀(X2)(SET(X2)→(¬ELEMENT(X2,X1))));
05500	
05600	∀(X1,X2)(DISJOINT(X1,X2)↔∀(X3)(SET(X3)→¬(ELEMENT(X3,X1)∧ELEMENT(X3,X2))));
05700	
05800	∀(X1)(ONEMANY(X1)↔∀(X2)(SET(X2)→∀(X3)(SET(X3)→∀(X4)(SET(X4)→
05900	((ELEMENT(TUPLE2(X3,X2),X1)∧ELEMENT(TUPLE2(X4,X2),X1))→EQU(X3,X4))))));;
06000	
06100	;
06200	
06300	∀(X1)(SET(X1) → ¬ELEMENT(X1,X1));;